\begin{tabbing}
$\forall$$T$:Type, ${\it ll}$:($T$ List) List, $x$:$T$.
\\[0ex]($x$ $\in$ concat(${\it ll}$))
\\[0ex]$\Leftrightarrow$
\\[0ex](\=$\exists$${\it ll}_{1}$, ${\it ll}_{2}$:($T$ List) List, $l_{1}$, $l_{2}$:$T$ List.\+
\\[0ex]concat(${\it ll}$) $=$ (concat(${\it ll}_{1}$) @ ($l_{1}$ @ [$x$] @ $l_{2}$) @ concat(${\it ll}_{2}$)) $\in$ $T$ List
\\[0ex]\& ${\it ll}$ $=$ (${\it ll}_{1}$ @ [$l_{1}$ @ [$x$] @ $l_{2}$] @ ${\it ll}_{2}$))
\-
\end{tabbing}